As mentioned in chapter~\ref{sec:intro_statement} we would like to understand
under which conditions it is possible that the behavioral description and the
access control policy of a system evolve such that, for an evolution step
changing model $n-1$ into model $n$, the permissions and prohibitions enforced
by the model $n-1$ are preserved by model $n$. The work presented in this paper
is heavily influenced by the studies on resilience presented in~\cite{lucio:10}.

As we have presented in chapter~\ref{sec:models_acp}, we are able to check if a
given algebraic Petri net model representing the behavioral description of a
system verifies permissions and prohibitions given by an access control policy.
This is done by transforming permissions and prohibitions into semantically
equivalent safety and reachability properties and the using a model checker to
verify the satisfaction of those properties in the model. We are thus interested
in understanding what kind of algebraic Petri net transformations preserve
safety and reachability properties as such a study will hopefully provide us
useful transformations for co-evolution of algebraic Petri nets and access
control policies.

The kind of transformations we will consider between two networks $N_1$ and
$N_2$ assume there is a total injective mapping between the places of $N_1$ and
those of $N_2$, as well as a total injective mapping between the transitions of
$N_1$ and those of $N_2$. They also require the arcs between the mapped places
and mapped transitions are preserved by the mappings. The mapping of $N_1$ can
be nonetheless be embedded into a larger $N_2$, under certain conditions. The
mappings described above are necessary for two reasons: 1) in order preserve the
semantics of $N_1$ in $N_2$; 2) in order to allow the transformation of the
safety and reachability properties themselves which are originally expressed in
terms of net $N_1$ and after the transformation should be verifiable over net
$N_2$. Notice that without such conditions for the transformation the semantics
of network $N_1$ or of the properties themselves would be lost during the
transformation and the result of verifying the transformed properties would not
be meaningful.

Let us now further define the conditions that allow embedding the mapping of a
network $N_1$ into a network $N_2$. If the goal is to preserve safety
properties, then additional input and output arcs of $N_2$ are allowed into the
mapped transitions of $N_1$\marginpar{output arcs of mapped places???}. It is
also possible to strengthen guard conditions of mapped transitions. The
intuition behind these embedding conditions is that additional conditions to
mapped transitions does not invalidate safety properties -- in fact by
restricting the flow of tokens harmful events continue not happening. On the
other hand adding input arcs to mapped places is not allowed as this could
violate the safety conditions on those places. The formal mathematical proofs
that such embeddings do in fact preserve safety properties can be found
in~\cite{lucio:10,Padberg97refinementversus}.

On the other hand, if the goal is to preserve reachability properties then the
embedding conditions are as follows: additional output arcs are allowed for any
mapped transition, as well as additional input and/or output arcs for any mapped
place. Also, condition weakening for any mapped transition is allowed. The
intuition behind these embedding conditions is that the token flow in the
embedded net cannot be constrained. However, additional tokens are permitted. As
such, no additional conditions for mapped transitions are allowed, in particular
by adding input arcs to mapped transitions or by transition guard strengthening.
Transition guard weakening is however possible. Again, the formal mathematical
proofs that such embeddings preserve reachability are described
in~\cite{lucio_reach:11,Padberg97refinementversus}.


\begin{itemize}
  \item APN transformations to preserve safety
  \item APN transformations to preserve reachability
  \item Model checking the opposite property
  \item Induced methodology
\end{itemize}